Nuprl Definition : interleaving
11,40
postcript
pdf
interleaving(
T
;
L1
;
L2
;
L
) == ||
L
|| = ||
L1
||+||
L2
|| & disjoint_sublists(
T
;
L1
;
L2
;
L
)
latex
clarification:
interleaving(
T
;
L1
;
L2
;
L
) == ||
L
|| = ||
L1
||+||
L2
||
& disjoint_sublists(
T
;
L1
;
L2
;
L
)
latex
Definitions
P
&
Q
,
s
=
t
,
,
n
+
m
,
||
as
||
,
disjoint_sublists(
T
;
L1
;
L2
;
L
)
FDL editor aliases
interleaving
origin
& disjoint_sublists(T;L1;L2;L) & disjoint_sublists(T;L1;L2;L)